R-Feasible{i:l}
R-Feasible(Rplus(ecl-machine{ecl:ut2}
R-Feasible(Rplus(ecl-machine(mkid{b:ut2};
R-Feasible(Rplus(ecl-machine(fpf-join(id-deq;
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-single(mkid{x1:ut2}; int_seg(0; 3));
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(id-deq;
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-single(mkid{v1:ut2}; int_seg(0; 3));
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-join(id-deq;
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-join(fpf-single(mkid{win:ut2}; );
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-join(fpf-join(id-deq;
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-join(fpf-join(fpf-single(mkid{x2:ut2};
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-join(fpf-join(fpf-single(int_seg(0; 3));
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-join(fpf-join(fpf-single(mkid{v2:ut2};
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-join(fpf-join(fpf-single(int_seg(0; 3))))));
R-Feasible(Rplus(ecl-machine(fpf-join(Kind-deq;
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(Kind-deq;
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-single(rcv(mklnk{input:ut2, b:ut2, 1:ut2
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-single(rcv(mklnk{},mkid{play:ut2});
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-single(int_seg(0; 3));
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-single(locl(mkid{choose1:ut2});
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-single(p-outcome(ternary-fps)));
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(Kind-deq;
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-single(locl(mkid{diff:ut2}); int_seg(0; 1));
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-join(Kind-deq;
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-join(fpf-single(locl(mkid{same:ut2});
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-join(fpf-single(int_seg(0; 1));
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-join(fpf-single(rcv(mklnk{b:ut2,
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-join(fpf-single(rcv(mklnk{output:ut2,
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-join(fpf-single(rcv(mklnk{1:ut2
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-join(fpf-single(rcv(mklnk{},mkid{hello:ut2});
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-join(fpf-single())));
R-Feasible(Rplus(ecl-machine(eclact(eclcatch(eclrepeat
R-Feasible(Rplus(ecl-machine(eclact(eclcatch((eclseq(ecland(eclbase(rcv(mklnk{input:ut2,
R-Feasible(Rplus(ecl-machine(eclact(eclcatch((eclseq(ecland(eclbase(rcv(mklnk{b:ut2,
R-Feasible(Rplus(ecl-machine(eclact(eclcatch((eclseq(ecland(eclbase(rcv(mklnk{1:ut2
R-Feasible(Rplus(ecl-machine(eclact(eclcatch((eclseq(ecland(eclbase(rcv(mklnk{},mkid{play:ut2});
R-Feasible(Rplus(ecl-machine(eclact(eclcatch((eclseq(ecland(eclbase((s,v. tt));
R-Feasible(Rplus(ecl-machine(eclact(eclcatch((eclseq(ecland(eclbase(locl(mkid{choose1:ut2});
R-Feasible(Rplus(ecl-machine(eclact(eclcatch((eclseq(ecland(eclbase((s,v. tt)));
R-Feasible(Rplus(ecl-machine(eclact(eclcatch((eclseq(eclor(eclthrow(eclbase(locl(mkid{diff:ut2});
R-Feasible(Rplus(ecl-machine(eclact(eclcatch((eclseq(eclor(eclthrow(eclbase((s,v. tt));
R-Feasible(Rplus(ecl-machine(eclact(eclcatch((eclseq(eclor(eclthrow(1);
R-Feasible(Rplus(ecl-machine(eclact(eclcatch((eclseq(eclor(eclbase(locl(mkid{same:ut2}); (s,v. tt))
R-Feasible(Rplus(ecl-machine(eclact(eclcatch((eclseq(eclor()));
R-Feasible(Rplus(ecl-machine(eclact(eclcatch(cons(1; []));
R-Feasible(Rplus(ecl-machine(eclact(1);
R-Feasible(Rplus(ecl-machine(msg-spec1(locl(mkid{diff:ut2});
R-Feasible(Rplus(ecl-machine(msg-spec1(mklnk{b:ut2, output:ut2, 1:ut2};
R-Feasible(Rplus(ecl-machine(msg-spec1(mkid{hello:ut2};
R-Feasible(Rplus(ecl-machine(msg-spec1(1;
R-Feasible(Rplus(ecl-machine(msg-spec1(s,v.rps((s(mkid{x1:ut2})); (s(mkid{v1:ut2}))));
R-Feasible(Rplus(ecl-machine(update-spec1(locl(mkid{diff:ut2});
R-Feasible(Rplus(ecl-machine(update-spec1(mkid{win:ut2};
R-Feasible(Rplus(ecl-machine(update-spec1(1;
R-Feasible(Rplus(ecl-machine(update-spec1(s,v.((s(mkid{win:ut2}))
R-Feasible(Rplus(ecl-machine(update-spec1(+ if rps((s(mkid{x1:ut2})); (s(mkid{v1:ut2})))
R-Feasible(Rplus(ecl-machine(update-spec1(+ then 1
R-Feasible(Rplus(ecl-machine(update-spec1(+ else 0
R-Feasible(Rplus(ecl-machine(update-spec1(+ fi )));
R-Feasible(Rplus(Rplus(Rplus(Rpre(mkid{b:ut2};
R-Feasible(Rplus(Rplus(Rplus(Rpre(fpf-join(id-deq;
R-Feasible(Rplus(Rplus(Rplus(Rpre(fpf-join(fpf-single(mkid{x1:ut2}; int_seg(0; 3));
R-Feasible(Rplus(Rplus(Rplus(Rpre(fpf-join(fpf-single(mkid{v1:ut2}; int_seg(0; 3)));
R-Feasible(Rplus(Rplus(Rplus(Rpre(mkid{diff:ut2};
R-Feasible(Rplus(Rplus(Rplus(Rpre(unit-fps;
R-Feasible(Rplus(Rplus(Rplus(Rpre((s.(s(mkid{x1:ut2}) = s(mkid{v1:ut2}))));
R-Feasible(Rplus(Rplus(Rplus(Rpre(mkid{b:ut2};
R-Feasible(Rplus(Rplus(Rplus(Rpre(fpf-join(id-deq;
R-Feasible(Rplus(Rplus(Rplus(Rpre(fpf-join(fpf-single(mkid{x1:ut2}; int_seg(0; 3));
R-Feasible(Rplus(Rplus(Rplus(Rpre(fpf-join(fpf-single(mkid{v1:ut2}; int_seg(0; 3)));
R-Feasible(Rplus(Rplus(Rplus(Rpre(mkid{same:ut2};
R-Feasible(Rplus(Rplus(Rplus(Rpre(unit-fps;
R-Feasible(Rplus(Rplus(Rplus(Rpre((s.(s(mkid{x1:ut2}) = s(mkid{v1:ut2})))));
R-Feasible(Rplus(Rplus(Rplus(Rpre(mkid{b:ut2}; fpf-empty; mkid{choose1:ut2}; ternary-fps; (s.tt));
R-Feasible(Rplus(Rplus(Rplus(Rplus(Reffect(mkid{b:ut2};
R-Feasible(Rplus(Rplus(Rplus(Rplus(Reffect(fpf-single(mkid{x1:ut2}; int_seg(0; 3));
R-Feasible(Rplus(Rplus(Rplus(Rplus(Reffect(rcv(mklnk{input:ut2, b:ut2, 1:ut2},mkid{play:ut2});
R-Feasible(Rplus(Rplus(Rplus(Rplus(Reffect(int_seg(0; 3);
R-Feasible(Rplus(Rplus(Rplus(Rplus(Reffect(mkid{x1:ut2};
R-Feasible(Rplus(Rplus(Rplus(Rplus(Reffect((inl (s,v. v) ));
R-Feasible(Rplus(Rplus(Rplus(Rplus(Reffect(mkid{b:ut2};
R-Feasible(Rplus(Rplus(Rplus(Rplus(Reffect(fpf-single(mkid{v1:ut2}; int_seg(0; 3));
R-Feasible(Rplus(Rplus(Rplus(Rplus(Reffect(locl(mkid{choose1:ut2});
R-Feasible(Rplus(Rplus(Rplus(Rplus(Reffect(p-outcome(ternary-fps);
R-Feasible(Rplus(Rplus(Rplus(Rplus(Reffect(mkid{v1:ut2};
R-Feasible(Rplus(Rplus(Rplus(Rplus(Reffect((inl (s,v. v) ))))))) 

latex

Definitions

locl_rcv{locl_rcv_compseq_tag_def:ObjectId}(tg; l; a), eq_lnk(a; b), idlnk-deq, product-deq(A; B; a; b), proddeq(a; b), rcv_rcv{rcv_rcv_compseq_tag_def:ObjectId}(t'; l'; t; l), deq-member(eq; x; L), ecl-kinds(x), ecl ind eclact compseq tag def, ecl ind eclcatch compseq tag def, ecl ind eclrepeat compseq tag def, ecl ind eclseq compseq tag def, ecl ind ecland compseq tag def, ecl ind eclor compseq tag def, ecl ind eclthrow compseq tag def, ecl ind eclbase compseq tag def, update-spec-vars(upd), locl_locl{locl_locl_compseq_tag_def:ObjectId}(b; a), rationals, decl-type{i:l}(ds; x), rcv_locl{rcv_locl_compseq_tag_def:ObjectId}(a; tg; l), R-loc(R), Rds(R), Rda(R), R-base-domain(R), eq_bd(p; q), R-frame-compat(A; B), R-interface-compat(A; B), Rplus?(x1), Rplus-left(x1), Rplus-right(x1), Rnone?(x1), Rframe?(x1), Rframe-x(x1), Rframe-L(x1), Raframe?(x1), Raframe-k(x1), Raframe-L(x1), Reffect-ds(x1), Rsframe?(x1), Rsframe-lnk(x1), Rsframe-tag(x1), Rsends-g(x1), Rsframe-L(x1), Rbframe?(x1), Rbframe-k(x1), Rbframe-L(x1), Rsends-ds(x1), Rpre?(x1), Rrframe?(x1), Rrframe-x(x1), Rpre-ds(x1), Rpre-a(x1), Rrframe-L(x1), Reffect-knd(x1), Reffect-T(x1), Rsends?(x1), Rsends-knd(x1), Rsends-l(x1), Rsends-dt(x1), Rsends-T(x1), (i = j), unit-fps, fpf-compatible(A; a.B(a); eq; f; g), R-discrete_compat(A; B), Reffect-discrete(A), Rinit-discrete(A), Reffect?(x1), Reffect-x(x1), Reffect-f(x1), Rinit?(x1), Rinit-x(x1), Rinit-v(x1), fpf-all(A; eq; f; x,v.P(x;v)), es_realizer{i:l}, rec(x.A(x)), finite-prob-space, update-spec(ds; da), t.2, update-spec1(k; x; n; s,v.f(s;v)), n + m, f(a), fpf-ap(f; eq; x), lelt(i; j; k), l_all(L; T; x.P(x)), if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), fpf-dom(eq; x; f), x:A. B(x), decidable(P), P  Q, isrcv(k), ||as||, tl(l), l[i], i z j, i <z j, hd(l), t.1, token{$x:ut2}, atom, source(l), top, isect(A; x.B(x)), A c B, inr x , eqof(d), atom2-deq, eq_atom{$n:n}(x; y), Reffect(loc; ds; knd; T; x; f), inl x , fpf-empty, Rplus(left; right), Rpre(loc; ds; a; p; P), ecl-machine{$ecl:ut2}(i; ds; da; A; snd; upd), R-has-loc(R; i), left + right, Unit, b, eq_id(a; b), atom{$n:n}, sqequal(s; t), prop{i:l}, sq_type(T), guard(T), P  Q, P  Q, P  Q, True, ternary-fps, x. t(x), Type, <a, b>, eclact(a; n), eclcatch(a; l), eclrepeat(a), eclseq(a; b), ecland(a; b), eclor(a; b), eclthrow(a; n), eclbase(k; test), tt, cons(car; cdr), [], #$n, , A, False, P  Q, a < b, A  B, decl-state(ds), x.A(x), ma-valtype(da; k), fpf-cap(f; eq; x; z), void, msg-spec(ds; da), fpf(A; a.B(a)), x:AB(x), msg-item(ds; da; k; l), {x:A| B(x)} , (x  l), type List, x:A  B(x), IdLnk, rps(x; y), msg-spec1(k; l; tg; n; s,v.f(s;v)), , Kind-deq, p-outcome(p), locl(a), rcv(l,tg), Knd, fpf-join(eq; f; g), id-deq, , fpf-single(x; v), int_seg(i; j), mkid{$x:ut2}, Id, x:A. B(x), x,y. t(x;y), t  T, mklnk{$a:ut2, $b:ut2, $n:ut2}, destination(l), es realizer ind Rpre compseq tag def, es realizer ind Rplus compseq tag def, es realizer ind Reffect compseq tag def, isrcv_rcv{isrcv_rcv_compseq_tag_def:ObjectId}(tg; l), lnk_rcv{lnk_rcv_compseq_tag_def:ObjectId}(tg; l), isrcv_locl{isrcv_locl_compseq_tag_def:ObjectId}(a), normal-ds{i:l}(ds), normal-type{i:l}(T), s = t, R-compat{i:l}(A; B), R-Feasible{i:l}(R), es realizer ind, b

Lemmas

msg-spec1 wf, rps wf, le wf, nat wf, ma-valtype wf, btrue wf, locl wf, eclbase wf, eclthrow wf, eclor wf, decl-state wf, rcv wf, ecland wf, eclseq wf, eclrepeat wf, eclcatch wf, eclact wf, bool wf, fpf-single wf, fpf-join wf, int seg wf, Kind-deq wf, ternary-fps wf, p-outcome wf, Knd wf, id-deq wf, Id wf, update-spec1-decl, ecl-machine wf, R-compat-Rplus-sq, R-compat-symmetry, Id sq, eq id wf, assert wf, not wf, bnot wf, assert-eq-id, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, ecl-machine-loc, R-compat-disjoint, ecl-disjoint-compatible, normal-ds-single, normal-ds-join, R-Feasible-Rplus, true wf, l member wf, length wf1, select wf, isrcv wf, decidable int equal, Knd sq, decidable equal Kind, decidable or, fpf-dom wf, top wf, fpf-single-dom, or functionality wrt iff, fpf-join-dom2, IdLnk wf, normal-da-single, normal-da-join, subtype rel self, eqof eq btrue, fpf-single-dom-sq, fpf-cap-single, fpf-join-cap-sq, fpf-cap-single-join, ifthenelse wf, update-spec1 wf, update-spec1 wf2, msg-spec-loc-decl-spec1, ecl-feasible, bool-inhabited, natural number wf p-outcome, length wf nat, false wf, Rpre wf, Reffect wf, Rplus wf, fpf-empty wf, fpf-all-empty, unit-fps wf, fpf-compatible-singles, fpf-compatible-symmetry, fpf-compatible-self, assert-eq-knd, fpf-empty-compatible-right, fpf-cap-single1, decl-type wf, rationals wf, eq int wf, fpf-compatible-join, fpf-empty-compatible-left, ecl-precond-compatible, fpf-compatible-join2, ecl-effect-compatible, deq-member wf, assert-deq-member